Small fix and some cleaning in nondet-static [TG-2755] #2874
Conversation
majakusber
requested review from
cesaro,
chrisr-diffblue,
cristina-david,
martin-cs,
mgudemann,
NathanJPhillips,
peterschrammel,
pkesseli,
smowton and
thk123
as code owners
This label is recognized by nondet-static option
majakusber
force-pushed
the
nondet_static_condition
branch
from
15423ea to
d97e9ff
Compare
| @@ -18,6 +18,44 @@ Date: November 2011 | |||
|
|
|||
| #include <linking/static_lifetime_init.h> | |||
|
|
|||
| /// Returns true if the symbol expression holds a static symbol that can be | |||
There was a problem hiding this comment.
shouldn't this be in \return ?
| /// Nondeterministically initializes certain global scope variables in | ||
| /// CPROVER_initialize function. | ||
| /// \param ns Namespace for resolving type information. | ||
| /// \param goto_functions Existing goto-functions to be updated. |
| @@ -49,7 +49,13 @@ bool is_nondet_initializable_static( | |||
| !is_constant_or_has_constant_components(ns.lookup(id).type, ns); | |||
| } | |||
|
|
|||
|
|
|||
| /// Nondeterministically initializes certain global scope variables in a | |||
There was a problem hiding this comment.
Not your fault but "certain" is very vague 🌵
| @@ -93,6 +99,10 @@ void nondet_static( | |||
| } | |||
| } | |||
|
|
|||
| /// Nondeterministically initializes certain global scope variables in | |||
| @@ -18,6 +18,38 @@ Date: November 2011 | |||
|
|
|||
| #include <linking/static_lifetime_init.h> | |||
|
|
|||
| /// Returns true if the symbol expression holds a static symbol that can be | |||
There was a problem hiding this comment.
⛏️ ⛏️ "that" -> "which"
|
Wishlist request: the PR title claims a bug is being fixed (and I think it's the first of the three commits doing so) - could a test be added that showcases the problem/works now while it didn't work before? It's perfectly possible that this can only be tested in some other code base such as TG and you might have a test in there, then all is well. Else I'd ask for a test to be added somewhere. |
|
@tautschnig Yes, the first commit is the bug fix. I needed to make this change because under the changes in my PR https://github.com/diffblue/test-gen/pull/2219 one of the regression tests is failing without it, namely All of the changes here actually came out of the work in https://github.com/diffblue/test-gen/pull/2219. I have a separate test-gen pointer bump for this so that I don't have to wait until all review comments are addressed on https://github.com/diffblue/test-gen/pull/2219. |
majakusber
force-pushed
the
nondet_static_condition
branch
from
d97e9ff to
4d0e23b
Compare
| if(!ns.get_symbol_table().has_symbol(id)) | ||
| return false; | ||
|
|
||
| // any other internal variable such as Java specific? |
There was a problem hiding this comment.
Would the comment be better saying something like "is the type explicitly marked as not to be nondet initialized?" I assume other language front-ends could conceivably also want to mark some types in the same way, so it might be nice not to make this sound too Java centric.
There was a problem hiding this comment.
I agree - this is not necessarily Java specific.
| if(!ns.get_symbol_table().has_symbol(id)) | ||
| return false; | ||
|
|
||
| // any other internal variable such as Java specific? |
There was a problem hiding this comment.
I agree - this is not necessarily Java specific.
| Module: Nondeterministic initialization of certain global scope | ||
| variables | ||
| Module: Nondeterministically initializes global scope variables, except for | ||
| constants (such as string literals, final fields) and internal variables |
There was a problem hiding this comment.
Please move the detailed description to the doxygen below.
So that the function can be called from other files too
majakusber
force-pushed
the
nondet_static_condition
branch
from
4d0e23b to
8230504
Compare
Fixing a small bug - adding a label to not nondet-initialize a Java internal variable, pulls out a function to make it available outside of the files and adds missing documentation.